*****ASSUME x≤y;

1 x≤y  (1)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY LOGICTREE∪{ TAK0,TAK1,1};

2 tak1(x,y,z)=tak0(x,y,z)  (1)

*****⊃I ↑↑⊃↑;

3 x≤y⊃tak1(x,y,z)=tak0(x,y,z)  

*****ASSUME ¬(x≤y);

4 ¬(x≤y)  (4)

*****∀E LESS2 x,y;

5 (x<y∧(¬(x=y)∧¬(y<x)))∨((¬(x<y)∧(x=y∧¬(y<x)))∨(¬(x<y)∧(¬(x=y)∧y<x)))  

*****∀E LESS4 x,y;

6 x≤y≡(x<y∨x=y)  

*****TAUT y<x 4:6;

7 y<x  (4)

*****ASSUME y≤z;

8 y≤z  (8)

*****∀E LESS1 y;

9 pred y<y  

*****∀E LESS3 pred y,y,z;

10 ((pred y<y∧y<z)⊃pred y<z)∧(((pred y≤y∧y<z)⊃pred y<z)∧(((pred y<y∧y≤z)⊃pred y<z)∧((pred y≤y∧y≤z)⊃pred y≤z)))  

*****∀E LESS4 pred y,y;

11 pred y≤y≡(pred y<y∨pred y=y)  

*****TAUT pred y≤z 8:11;

12 pred y≤z  (8)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY LOGICTREE∪{ TAK0,TAK1,4,7:8,12};

13 tak1(x,y,z)=tak0(x,y,z)≡IF IF pred x≤y THEN y ELSE z≤z THEN z ELSE IF z≤IF pred z≤x THEN x ELSE pred z THEN I%
F pred z≤x THEN x ELSE pred z ELSE IF pred x≤y THEN y ELSE z=z  (4 8)

*****ASSUME pred x≤y;

14 pred x≤y  (14)

*****REWRITE ↑↑ BY LOGICTREE∪{ 8,14};

15 tak1(x,y,z)=tak0(x,y,z)  (4 8 14)

*****⊃I ↑↑⊃↑;

16 pred x≤y⊃tak1(x,y,z)=tak0(x,y,z)  (4 8)

*****ASSUME ¬(pred x≤y);

17 ¬(pred x≤y)  (17)

*****REWRITE 13 BY LOGICTREE∪{ LESS4,8,17};

18 tak1(x,y,z)=tak0(x,y,z)  (4 8 17)

*****⊃I ↑↑⊃↑;

19 ¬(pred x≤y)⊃tak1(x,y,z)=tak0(x,y,z)  (4 8)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 16,19;

20 tak1(x,y,z)=tak0(x,y,z)  (4 8)

*****ASSUME ¬(y≤z);

21 ¬(y≤z)  (21)

*****∀E LESS2 y,z;

22 (y<z∧(¬(y=z)∧¬(z<y)))∨((¬(y<z)∧(y=z∧¬(z<y)))∨(¬(y<z)∧(¬(y=z)∧z<y)))  

*****∀E LESS4 y,z;

23 y≤z≡(y<z∨y=z)  

*****TAUT z<y 21:23;

24 z<y  (21)

*****∀E LESS1 z;

25 pred z<z  

*****∀E LESS3 pred z,z,y;

26 ((pred z<z∧z<y)⊃pred z<y)∧(((pred z≤z∧z<y)⊃pred z<y)∧(((pred z<z∧z≤y)⊃pred z<y)∧((pred z≤z∧z≤y)⊃pred z≤y)))  

*****∀E LESS4 pred z,z;

27 pred z≤z≡(pred z<z∨pred z=z)  

*****∀E LESS4 pred z,y;

28 pred z≤y≡(pred z<y∨pred z=y)  

*****TAUT pred z≤y 24:28;

29 pred z≤y  (21)

*****∀E LESS3 z,y,x;

30 ((z<y∧y<x)⊃z<x)∧(((z≤y∧y<x)⊃z<x)∧(((z<y∧y≤x)⊃z<x)∧((z≤y∧y≤x)⊃z≤x)))  

*****∀E LESS4 z,y;

31 z≤y≡(z<y∨z=y)  

*****∀E LESS4 y,x;

32 y≤x≡(y<x∨y=x)  

*****TAUT z≤x 7,24,30:32;

33 z≤x  (4 21)

*****∀E LESS3 pred z,y,x;

34 ((pred z<y∧y<x)⊃pred z<x)∧(((pred z≤y∧y<x)⊃pred z<x)∧(((pred z<y∧y≤x)⊃pred z<x)∧((pred z≤y∧y≤x)⊃pred z≤x)))  

*****TAUT pred z≤x 7,29,32,34;

35 pred z≤x  (4 21)

*****REWRITE tak1(x,y,z)=tak0(x,y,z) BY LOGICTREE∪{ TAK0,TAK1,4,21,29,33,35};

36 tak1(x,y,z)=tak0(x,y,z)≡IF IF pred x≤y THEN y ELSE pred x≤IF pred y≤z THEN z ELSE x THEN IF pred y≤z THEN z E%
LSE x ELSE IF IF pred y≤z THEN z ELSE x≤x THEN x ELSE IF pred x≤y THEN y ELSE pred x=x  (4 21)

*****ASSUME pred x≤y;

37 pred x≤y  (37)

*****ASSUME pred y≤z;

38 pred y≤z  (38)

*****REWRITE ↑↑↑ BY LOGICTREE∪{ 21,33,37:38};

39 tak1(x,y,z)=tak0(x,y,z)  (4 21 37 38)

*****ASSUME ¬(pred x≤y);

40 ¬(pred x≤y)  (40)

*****REWRITE 36 BY LOGICTREE∪{ 33,38,40};

41 tak1(x,y,z)=tak0(x,y,z)≡IF pred x≤z THEN z ELSE x=x  (4 21 38 40)

*****∀E LESS3 pred x,z,y;

42 ((pred x<z∧z<y)⊃pred x<y)∧(((pred x≤z∧z<y)⊃pred x<y)∧(((pred x<z∧z≤y)⊃pred x<y)∧((pred x≤z∧z≤y)⊃pred x≤y)))  

*****∀E LESS4 pred x,y;

43 pred x≤y≡(pred x<y∨pred x=y)  

*****TAUT ¬(pred x≤z) 24,40,42:43;

44 ¬(pred x≤z)  (21 40)

*****REWRITE 41 BY LOGICTREE∪{ 44};

45 tak1(x,y,z)=tak0(x,y,z)  (4 21 38 40)

*****⊃I 37⊃39;

46 pred x≤y⊃tak1(x,y,z)=tak0(x,y,z)  (4 21 38)

*****⊃I 40⊃↑↑;

47 ¬(pred x≤y)⊃tak1(x,y,z)=tak0(x,y,z)  (4 21 38)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 46:47;

48 tak1(x,y,z)=tak0(x,y,z)  (4 21 38)

*****ASSUME ¬(pred y≤z);

49 ¬(pred y≤z)  (49)

*****∀E LESS1 x;

50 pred x<x  

*****REWRITE 36 BY LOGICTREE∪{ 37,49:50};

51 tak1(x,y,z)=tak0(x,y,z)≡IF y≤x THEN x ELSE IF x≤x THEN x ELSE y=x  (4 21 37 49)

*****TAUT y≤x 7,32;

52 y≤x  (4)

*****REWRITE ↑↑ BY LOGICTREE∪{ 52};

53 tak1(x,y,z)=tak0(x,y,z)  (4 21 37 49)

*****REWRITE 36 BY LOGICTREE∪{ 40,49:50};

54 tak1(x,y,z)=tak0(x,y,z)≡IF pred x≤x THEN x ELSE IF x≤x THEN x ELSE pred x=x  (4 21 40 49)

*****∀E LESS4 pred x,x;

55 pred x≤x≡(pred x<x∨pred x=x)  

*****TAUT pred x≤x 50,55;

56 pred x≤x  

*****REWRITE ↑↑↑ BY LOGICTREE∪{ 56};

57 tak1(x,y,z)=tak0(x,y,z)  (4 21 40 49)

*****⊃I 37⊃53;

58 pred x≤y⊃tak1(x,y,z)=tak0(x,y,z)  (4 21 49)

*****⊃I 40⊃↑↑;

59 ¬(pred x≤y)⊃tak1(x,y,z)=tak0(x,y,z)  (4 21 49)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 58:59;

60 tak1(x,y,z)=tak0(x,y,z)  (4 21 49)

*****⊃I 49⊃↑;

61 ¬(pred y≤z)⊃tak1(x,y,z)=tak0(x,y,z)  (4 21)

*****⊃I 38⊃48;

62 pred y≤z⊃tak1(x,y,z)=tak0(x,y,z)  (4 21)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 61:62;

63 tak1(x,y,z)=tak0(x,y,z)  (4 21)

*****⊃I 21⊃↑;

64 ¬(y≤z)⊃tak1(x,y,z)=tak0(x,y,z)  (4)

*****⊃I 8⊃20;

65 y≤z⊃tak1(x,y,z)=tak0(x,y,z)  (4)

*****TAUT tak1(x,y,z)=tak0(x,y,z) 64:65;

66 tak1(x,y,z)=tak0(x,y,z)  (4)

*****⊃I 4⊃↑;

67 ¬(x≤y)⊃tak1(x,y,z)=tak0(x,y,z)  

*****TAUT tak1(x,y,z)=tak0(x,y,z) 3,67;

68 tak1(x,y,z)=tak0(x,y,z)